$\forall$$E$:Type, $t$:Tree($E$). is\_leaf($t$) $\Rightarrow$ leaf\_value($t$) $\in$ $E$